Inference at * 2 2 2 
Iof proof for Lemma member-zip:



1. A : Type
2. B : Type
3. A List
4. u : A
5. v : A List
6. ys:(B List), x:A, y:B. (<x, y>  zip(v;ys))  {(x  v) & (y  ys)}
7. B List
8. u1 : B
9. v1 : B List
10. x:A, y:B. (<x, y>  zip([u / v];v1))  {(x  [u / v]) & (y  v1)}
11. x : A
12. y : B
13. (<x, y>  zip(v;v1))
  {(x  [u / v]) & (y  [u1 / v1])} 

latex

 by InstHyp [v1;x;y] 6 THENA Auto 
THEN Unfold `guard` 0 THEN RWO "cons_member" 0 THEN Auto 

THTHEN OrRight THEN Auto 

latex

TH.

Definitions	P  Q, x:A  B(x), P  Q, P  Q, x:AB(x), [car / cdr], P & Q, left + right, (x  l), P  Q, {T}, x:A. B(x), , s = t, t  T
Lemmas	and functionality wrt iff, cons member, l member wf